/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */
package chameleon.model.NuGatStructure.strategy;

import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.prop.Prop;
import chameleon.model.NuGatStructure.opt.Opt;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.fsm.FsmBuilder;
import chameleon.model.NuGatStructure.fsm.BddFsm;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.ClusterList;
import chameleon.model.NuGatStructure.bdd.ClusterOptions;
import chameleon.model.NuGatStructure.bdd.BddTrans;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.enc.BoolEnc;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.*;
import chameleon.model.NuGatStructure.fsm.SexpFsm;
import chameleon.model.game.Game;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;
import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.Hashtable;
import java.util.Vector;

/**
 * this class is a wrapper to the C struct GameStrategy.c
 * @author simon
 */
public abstract class GameStrategy extends NuGatStructure {
    
    protected PropGame prop_;    
    protected int reverseInitialQuantifiers_;
    protected BddEnc enc_ = null;
    private Vector<Bdd> bddVars_ = null;
    private Hashtable bddVarsIndex_ = null;

    public GameStrategy(Pointer structure, NuGatInterface nugat) {
        super(structure, nugat);
    }
    
    public GameStrategy (Pointer structure, PropGame prop, NuGatInterface nugat){
        super(structure,nugat);
        prop_ = prop;
    }
    
    //************************* DESTRUCTOR **********************************//
    
    public void destroy(){
        nugat_.GameStrategy_destroy(this.ptr());
    }
    
    /**
     * Print the strategy in the given file.      * 
     * @param file 
     */
    
    abstract public void printStrategy (String file);
    
    public void modifyVarOrder(String orderFile, BoolEnc boolEnc, Opt opt){
       checkStrategyExistence();
       BddEnc enc = getBddEnc(); 
       opt.setInputOrderFile(orderFile);
       
       Pointer ord_groups = nugat_.enc_utils_parse_ordering_file(opt.getInputOrderFile(), boolEnc.ptr());
       enc.forceOrder(ord_groups);
       enc_ = enc;
    }
    
    
    //*********************** GETTER ****************************************//
    
    public final int getReverseInitialQuantifiers(){
        checkStrategyExistence();
        return reverseInitialQuantifiers_;
    }
    
    public BddEnc getBddEnc(){
        checkStrategyExistence();
        if (enc_ == null)
            enc_ = new BddEnc(nugat_.GameStrategy_get_bdd_enc(this.ptr()),nugat_);
        return enc_; 
    }
    
    public GamePlayer getPlayer(){
        checkStrategyExistence();
        return new GamePlayer(nugat_.GameStrategy_get_player(this.ptr()),nugat_);
    }
    
    /**
     *  Synopsis    [ Getter for init_goal ]

        Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getInitGoal(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_init_goal(this.ptr()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for init_opponent_deadlock ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getInitOpponentDeadlock(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_init_opponent_deadlock(this.ptr()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for init_moves ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getInitMoves(){
        checkStrategyExistence();
        return new Bdd (nugat_.GameStrategy_get_init_moves(this.ptr()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for goal ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getGoal(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_goal(this.ptr()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for opponent_deadlock ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getOpponentDeadlock(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_opponent_deadlock(this.ptr()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for moves ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    public Bdd getMoves(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_moves(this.ptr()),nugat_);
    }
    
    /**
     * 
     * @return type of game on NuGaT format 
     */    
    public final int getType(){
        return prop_.getType();
    }
    
    protected Bdd getInitBdd(){
        BddEnc enc = getBddEnc();
        DdManager ddManager = enc.getDdManager();
        Bdd init =  ddManager.bddDup(getInitGoal());
        
        init = ddManager.bddOrAccumulate(init, getInitOpponentDeadlock());
        init = ddManager.bddOrAccumulate(init, getInitMoves());
        
        return init;
    }
    
    protected Bdd getTransBdd(){
        BddEnc enc = getBddEnc();
        DdManager ddManager = enc.getDdManager();
        Bdd trans = ddManager.bddDup(getGoal());
        
        trans = ddManager.bddOrAccumulate(trans, getOpponentDeadlock());
        trans = ddManager.bddOrAccumulate(trans, getMoves());
        
        
        return trans;
    }
    
    private BddTrans getTransBddTrans(FsmBuilder fsmBuilder, Opt opt){
        BddEnc enc = getBddEnc();
        DdManager ddManager = enc.getDdManager();
        ClusterList clusters;
        ClusterOptions clusterOptions;
        
        Node transExpr = enc.bddToExpr(getTransBdd());
        
        
        /* clusters construction */
        clusters = fsmBuilder.clusterizeExpr(
                enc,
                transExpr.ptr());
        
        clusterOptions = new ClusterOptions(opt, nugat_);
        
        
        BddTrans trans = new BddTrans(ddManager,
                                clusters,
                                enc.getStateVarsCube(),
                                ddManager.bddOne(),
                                enc.getNextStateVarsCube(),
                                opt.getPartitionMethod(),
                                clusterOptions,
                                nugat_);
        
        return trans;
    }
    
    /**
     * This function convert the winning stratefy for a player to a BddFsm
     * @param playerBddFsm
     * @return 
     */
    
    protected final BddFsm getBddFsm(BddFsm playerBddFsm, Opt opt, FsmBuilder fsmBuilder){
        
        BddTrans trans = getTransBddTrans(fsmBuilder, opt);
        
        
        BddFsm winningBddFsm = new BddFsm(enc_,
                getInitBdd(),
                playerBddFsm.getInvarStates(),
                playerBddFsm.getInvarInputs(),
                trans,
                playerBddFsm.getJustice(),
                playerBddFsm.getCompassion(), nugat_);
        
        
        return winningBddFsm;
    }
    
    protected final SexpFsm getSexpFsm(){
        return null;
    }
    
    public final PropGame getProp(){
        return prop_;
    }
    
    protected abstract Node getLtlSpec();
    
    public final int getSize(){
        checkStrategyExistence();
        int size = 0;
        DdManager dd = getBddEnc().getDdManager();
        size = dd.bddSize(getInitGoal()) + dd.bddSize(getInitMoves()) + dd.bddSize(getInitOpponentDeadlock())
                + dd.bddSize(getGoal())+dd.bddSize(getMoves())+dd.bddSize(getOpponentDeadlock());
        return size;
    }
    
    //************************* SETTER **************************************//
    
    public final void setReverseInitialQuantifiers(int reverseInitialQuantifiers_) {
        this.reverseInitialQuantifiers_ = reverseInitialQuantifiers_;
    }
    
    public void setInitGoal(Bdd initGoal){
        nugat_.GameStrategy_set_init_goal(this.ptr(), initGoal.ptr());
    }
    
    public void setInitOpponentDeadlock(Bdd initOpponentDeadlock){
        nugat_.GameStrategy_set_init_opponent_deadlock(this.ptr(), initOpponentDeadlock.ptr());
    }
    
    public void setInitMoves(Bdd initMoves){
        nugat_.GameStrategy_set_init_moves(this.ptr(), initMoves.ptr());
    }
    
    public void setGoal(Bdd goal){
        nugat_.GameStrategy_set_goal(this.ptr(), goal.ptr());
    }
    
    public void setOpponentDeadlock(Bdd opponentDeadlock){
        nugat_.GameStrategy_set_opponent_deadlock(this.ptr(), opponentDeadlock.ptr());
    }
    
    public void setMoves(Bdd moves){
        nugat_.GameStrategy_set_moves(this.ptr(), moves.ptr());
    }
    
    public final void setProp(PropGame prop){
        prop_ = prop;
    }

    public final void setBddVarsIndex(Hashtable bddVarsIndex_) {
        this.bddVarsIndex_ = bddVarsIndex_;
    }

    public final void setBddVars(Vector<Bdd> bddVars_) {
        this.bddVars_ = bddVars_;
    }

    public final void setEnc(BddEnc enc_) {
        this.enc_ = enc_;
    }
    
    
    
    //************************** METHOD *************************************//
    
    /**
     * Print result of strategy
     */
    
    public void printStatus() {
        
          OutputManager output = new OutputManager();
          output.displayString("Chameleon : ");
          Node exprCore = new Node (prop_.getExprCore().ptr(),nugat_);
          output.displayString(exprCore.sprintNode());
    }
    
    protected final void checkStrategyExistence(){
        if (!StrategyExists())
            throw new RuntimeException("No Strategy are encoded");
    }
    
    protected final boolean StrategyExists(){
        return (this.ptr() != Pointer.NULL);
    }

    public final void extractSubset(String maskFileName) throws IOException {
        checkStrategyExistence();
        DdManager ddManager = enc_.getDdManager();
        getBddVariables();
        /*int[] cubeArray = getCubeArray(maskFileName);
        Bdd cube = ddManager.CubeArrayToBdd(cubeArray);
        System.out.println("cube : "+cube.toString(enc_));*/
        Vector<Bdd> mask;
        
        mask = getMask(maskFileName); 
        
        Bdd bdd = this.getInitGoal();
        
        if (bddIsOk(bdd))
            this.setInitGoal(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
        
        bdd = this.getInitMoves();
        if (bddIsOk(bdd))
            this.setInitMoves(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
        
        bdd = this.getInitOpponentDeadlock();
        if (bddIsOk(bdd))
            this.setInitOpponentDeadlock(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
        
        bdd = this.getGoal();
        if (bddIsOk(bdd))
            this.setGoal(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
        
        bdd = this.getMoves();
        if (bddIsOk(bdd))
            this.setMoves(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
        
        bdd = this.getOpponentDeadlock();
        if (bddIsOk(bdd))
            this.setOpponentDeadlock(ddManager.existAbstract(ddManager.bddDup(bdd),mask));
       
    }
    
    private void getBddVariables(){
        if(bddVars_ == null){
            bddVars_ = new Vector<Bdd>();
            bddVarsIndex_ = new Hashtable();
              
            DdManager ddManager = enc_.getDdManager();
            int size = nugat_.dd_get_size(ddManager.ptr());
            
            Bdd var;
            
            for (int i=1; i < size; ++i ){
                var = ddManager.bddNewVarWithIndex(i);
                bddVars_.add(ddManager.bddDup(var));
                Node varExp = enc_.bddToExpr(var);
                bddVarsIndex_.put(varExp.sprintNode(), i);
            }
            
        }
    }

    private Vector<Bdd> getMask(String fileName) throws IOException{
        Vector<Bdd> mask = new Vector<Bdd>();
        DdManager ddManager = enc_.getDdManager();
        
        InputStream ips=new FileInputStream(fileName); 
        InputStreamReader ipsr=new InputStreamReader(ips);
	BufferedReader br=new BufferedReader(ipsr);
	String varName;
	while ((varName=br.readLine())!=null){
            Integer index =(Integer) bddVarsIndex_.get(varName);
            mask.add(ddManager.bddNewVarWithIndex(index));
            mask.add(ddManager.bddNewVarWithIndex(index+1));
	}
	br.close(); 
        return mask;
    }
    
    private int[] getCubeArray(String fileName) throws IOException{
        Vector<Integer> array = new Vector<Integer>();
        
        InputStream ips=new FileInputStream(fileName); 
        InputStreamReader ipsr=new InputStreamReader(ips);
	BufferedReader br=new BufferedReader(ipsr);
	String varName;
	while ((varName=br.readLine())!=null){
            Integer index =(Integer) bddVarsIndex_.get(varName);
            array.add(index);
            //We conserve the variable and the next variable.
            array.add(index+1);
	}
	br.close();
        
        int[] cube = new int[array.size()];
        
        for (int i=0; i < array.size(); ++i){
            cube[i] = array.get(i);
        }
        
        return cube;
    }

    /**
     * Return true if a bdd is not null, not equals to 1 and not equals to 0.
     * @param bdd
     * @return 
     */
    
    private boolean bddIsOk(Bdd bdd){
        DdManager ddManager = enc_.getDdManager();
        return (bdd.notNull() && !ddManager.bddIsOne(bdd)
                && !ddManager.bddIsZero(bdd));
    }

    public void strategyIsWinning(Game game){
        GamePlayer player = getPlayer();
        String strPlayer = player.toString();
        
        
        Node spec = getLtlSpec();
        
        BddFsm playerBddFsm;
        BddFsm opponentBddFsm;
        BddFsm stratBddFsm;
        
        if (strPlayer.equals(nugat_.PLAYER_NAME_1)){
            playerBddFsm = game.getBddFsmP1().clone();
            opponentBddFsm = game.getBddFsmP2().clone();
        }
        else{
            playerBddFsm = game.getBddFsmP2().clone();
            opponentBddFsm = game.getBddFsmP1().clone();
        }
        
        
        //create the strategy bdd fsm
        stratBddFsm = getBddFsm(playerBddFsm, game.getOptsHandlerInstance(),
                game.getGlobalFsmBuilder());
        
        //third Game * strategy
        opponentBddFsm.applySynchronousProduct(stratBddFsm);
        
        opponentBddFsm.checkLtlSpec(new Prop(spec, nugat_.Prop_Ltl, nugat_), game.getPropDatabase());
    }
}
